0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 187 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 116 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 15 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇔, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇔, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 PiDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 PiDP
↳33 PiDPToQDPProof (⇒, 4 ms)
↳34 QDP
↳35 Rewriting (⇔, 10 ms)
↳36 QDP
↳37 UsableRulesProof (⇔, 0 ms)
↳38 QDP
↳39 QReductionProof (⇔, 0 ms)
↳40 QDP
↳41 QDPOrderProof (⇔, 156 ms)
↳42 QDP
↳43 DependencyGraphProof (⇔, 0 ms)
↳44 QDP
↳45 UsableRulesProof (⇔, 0 ms)
↳46 QDP
↳47 QReductionProof (⇔, 0 ms)
↳48 QDP
↳49 QDPOrderProof (⇔, 68 ms)
↳50 QDP
↳51 DependencyGraphProof (⇔, 0 ms)
↳52 TRUE
gcdE_in_gga(s(T19), s(T20), T10) → U5_gga(T19, T20, T10, leA_in_gg(T19, T20))
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
U5_gga(T19, T20, T10, leA_out_gg(T19, T20)) → gcdE_out_gga(s(T19), s(T20), T10)
gcdE_in_gga(s(T51), s(T52), T54) → U6_gga(T51, T52, T54, leA_in_gg(T51, T52))
U6_gga(T51, T52, T54, leA_out_gg(T51, T52)) → U7_gga(T51, T52, T54, addD_in_gag(T51, X55, T52))
addD_in_gag(T72, X91, T73) → U4_gag(T72, X91, T73, addB_in_gag(T72, X91, T73))
addB_in_gag(s(T84), X115, s(T85)) → U2_gag(T84, X115, T85, addB_in_gag(T84, X115, T85))
addB_in_gag(0, T90, T90) → addB_out_gag(0, T90, T90)
U2_gag(T84, X115, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
U4_gag(T72, X91, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U7_gga(T51, T52, T54, addD_out_gag(T51, X55, T52)) → gcdE_out_gga(s(T51), s(T52), T54)
U6_gga(T51, T52, T54, leA_out_gg(T51, T52)) → U8_gga(T51, T52, T54, addD_in_gag(T51, T57, T52))
U8_gga(T51, T52, T54, addD_out_gag(T51, T57, T52)) → U9_gga(T51, T52, T54, gcdE_in_gga(s(T51), T57, T54))
gcdE_in_gga(0, s(T105), s(T105)) → gcdE_out_gga(0, s(T105), s(T105))
gcdE_in_gga(0, 0, 0) → gcdE_out_gga(0, 0, 0)
gcdE_in_gga(T115, T116, T118) → U10_gga(T115, T116, T118, gtC_in_gg(T115, T116))
gtC_in_gg(s(T131), s(T132)) → U3_gg(T131, T132, gtC_in_gg(T131, T132))
gtC_in_gg(s(T137), 0) → gtC_out_gg(s(T137), 0)
U3_gg(T131, T132, gtC_out_gg(T131, T132)) → gtC_out_gg(s(T131), s(T132))
U10_gga(T115, T116, T118, gtC_out_gg(T115, T116)) → gcdE_out_gga(T115, T116, T118)
gcdE_in_gga(T144, 0, T144) → U11_gga(T144, gtC_in_gg(T144, 0))
U11_gga(T144, gtC_out_gg(T144, 0)) → gcdE_out_gga(T144, 0, T144)
gcdE_in_gga(T152, s(T151), T154) → U12_gga(T152, T151, T154, gtC_in_gg(T152, s(T151)))
U12_gga(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U13_gga(T152, T151, T154, addB_in_gag(s(T151), X202, T152))
U13_gga(T152, T151, T154, addB_out_gag(s(T151), X202, T152)) → gcdE_out_gga(T152, s(T151), T154)
U12_gga(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U14_gga(T152, T151, T154, addB_in_gag(s(T151), T157, T152))
U14_gga(T152, T151, T154, addB_out_gag(s(T151), T157, T152)) → U15_gga(T152, T151, T154, gcdE_in_gga(s(T151), T157, T154))
U15_gga(T152, T151, T154, gcdE_out_gga(s(T151), T157, T154)) → gcdE_out_gga(T152, s(T151), T154)
U9_gga(T51, T52, T54, gcdE_out_gga(s(T51), T57, T54)) → gcdE_out_gga(s(T51), s(T52), T54)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
gcdE_in_gga(s(T19), s(T20), T10) → U5_gga(T19, T20, T10, leA_in_gg(T19, T20))
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
U5_gga(T19, T20, T10, leA_out_gg(T19, T20)) → gcdE_out_gga(s(T19), s(T20), T10)
gcdE_in_gga(s(T51), s(T52), T54) → U6_gga(T51, T52, T54, leA_in_gg(T51, T52))
U6_gga(T51, T52, T54, leA_out_gg(T51, T52)) → U7_gga(T51, T52, T54, addD_in_gag(T51, X55, T52))
addD_in_gag(T72, X91, T73) → U4_gag(T72, X91, T73, addB_in_gag(T72, X91, T73))
addB_in_gag(s(T84), X115, s(T85)) → U2_gag(T84, X115, T85, addB_in_gag(T84, X115, T85))
addB_in_gag(0, T90, T90) → addB_out_gag(0, T90, T90)
U2_gag(T84, X115, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
U4_gag(T72, X91, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U7_gga(T51, T52, T54, addD_out_gag(T51, X55, T52)) → gcdE_out_gga(s(T51), s(T52), T54)
U6_gga(T51, T52, T54, leA_out_gg(T51, T52)) → U8_gga(T51, T52, T54, addD_in_gag(T51, T57, T52))
U8_gga(T51, T52, T54, addD_out_gag(T51, T57, T52)) → U9_gga(T51, T52, T54, gcdE_in_gga(s(T51), T57, T54))
gcdE_in_gga(0, s(T105), s(T105)) → gcdE_out_gga(0, s(T105), s(T105))
gcdE_in_gga(0, 0, 0) → gcdE_out_gga(0, 0, 0)
gcdE_in_gga(T115, T116, T118) → U10_gga(T115, T116, T118, gtC_in_gg(T115, T116))
gtC_in_gg(s(T131), s(T132)) → U3_gg(T131, T132, gtC_in_gg(T131, T132))
gtC_in_gg(s(T137), 0) → gtC_out_gg(s(T137), 0)
U3_gg(T131, T132, gtC_out_gg(T131, T132)) → gtC_out_gg(s(T131), s(T132))
U10_gga(T115, T116, T118, gtC_out_gg(T115, T116)) → gcdE_out_gga(T115, T116, T118)
gcdE_in_gga(T144, 0, T144) → U11_gga(T144, gtC_in_gg(T144, 0))
U11_gga(T144, gtC_out_gg(T144, 0)) → gcdE_out_gga(T144, 0, T144)
gcdE_in_gga(T152, s(T151), T154) → U12_gga(T152, T151, T154, gtC_in_gg(T152, s(T151)))
U12_gga(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U13_gga(T152, T151, T154, addB_in_gag(s(T151), X202, T152))
U13_gga(T152, T151, T154, addB_out_gag(s(T151), X202, T152)) → gcdE_out_gga(T152, s(T151), T154)
U12_gga(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U14_gga(T152, T151, T154, addB_in_gag(s(T151), T157, T152))
U14_gga(T152, T151, T154, addB_out_gag(s(T151), T157, T152)) → U15_gga(T152, T151, T154, gcdE_in_gga(s(T151), T157, T154))
U15_gga(T152, T151, T154, gcdE_out_gga(s(T151), T157, T154)) → gcdE_out_gga(T152, s(T151), T154)
U9_gga(T51, T52, T54, gcdE_out_gga(s(T51), T57, T54)) → gcdE_out_gga(s(T51), s(T52), T54)
GCDE_IN_GGA(s(T19), s(T20), T10) → U5_GGA(T19, T20, T10, leA_in_gg(T19, T20))
GCDE_IN_GGA(s(T19), s(T20), T10) → LEA_IN_GG(T19, T20)
LEA_IN_GG(s(T33), s(T34)) → U1_GG(T33, T34, leA_in_gg(T33, T34))
LEA_IN_GG(s(T33), s(T34)) → LEA_IN_GG(T33, T34)
GCDE_IN_GGA(s(T51), s(T52), T54) → U6_GGA(T51, T52, T54, leA_in_gg(T51, T52))
U6_GGA(T51, T52, T54, leA_out_gg(T51, T52)) → U7_GGA(T51, T52, T54, addD_in_gag(T51, X55, T52))
U6_GGA(T51, T52, T54, leA_out_gg(T51, T52)) → ADDD_IN_GAG(T51, X55, T52)
ADDD_IN_GAG(T72, X91, T73) → U4_GAG(T72, X91, T73, addB_in_gag(T72, X91, T73))
ADDD_IN_GAG(T72, X91, T73) → ADDB_IN_GAG(T72, X91, T73)
ADDB_IN_GAG(s(T84), X115, s(T85)) → U2_GAG(T84, X115, T85, addB_in_gag(T84, X115, T85))
ADDB_IN_GAG(s(T84), X115, s(T85)) → ADDB_IN_GAG(T84, X115, T85)
U6_GGA(T51, T52, T54, leA_out_gg(T51, T52)) → U8_GGA(T51, T52, T54, addD_in_gag(T51, T57, T52))
U8_GGA(T51, T52, T54, addD_out_gag(T51, T57, T52)) → U9_GGA(T51, T52, T54, gcdE_in_gga(s(T51), T57, T54))
U8_GGA(T51, T52, T54, addD_out_gag(T51, T57, T52)) → GCDE_IN_GGA(s(T51), T57, T54)
GCDE_IN_GGA(T115, T116, T118) → U10_GGA(T115, T116, T118, gtC_in_gg(T115, T116))
GCDE_IN_GGA(T115, T116, T118) → GTC_IN_GG(T115, T116)
GTC_IN_GG(s(T131), s(T132)) → U3_GG(T131, T132, gtC_in_gg(T131, T132))
GTC_IN_GG(s(T131), s(T132)) → GTC_IN_GG(T131, T132)
GCDE_IN_GGA(T144, 0, T144) → U11_GGA(T144, gtC_in_gg(T144, 0))
GCDE_IN_GGA(T144, 0, T144) → GTC_IN_GG(T144, 0)
GCDE_IN_GGA(T152, s(T151), T154) → U12_GGA(T152, T151, T154, gtC_in_gg(T152, s(T151)))
GCDE_IN_GGA(T152, s(T151), T154) → GTC_IN_GG(T152, s(T151))
U12_GGA(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U13_GGA(T152, T151, T154, addB_in_gag(s(T151), X202, T152))
U12_GGA(T152, T151, T154, gtC_out_gg(T152, s(T151))) → ADDB_IN_GAG(s(T151), X202, T152)
U12_GGA(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U14_GGA(T152, T151, T154, addB_in_gag(s(T151), T157, T152))
U14_GGA(T152, T151, T154, addB_out_gag(s(T151), T157, T152)) → U15_GGA(T152, T151, T154, gcdE_in_gga(s(T151), T157, T154))
U14_GGA(T152, T151, T154, addB_out_gag(s(T151), T157, T152)) → GCDE_IN_GGA(s(T151), T157, T154)
gcdE_in_gga(s(T19), s(T20), T10) → U5_gga(T19, T20, T10, leA_in_gg(T19, T20))
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
U5_gga(T19, T20, T10, leA_out_gg(T19, T20)) → gcdE_out_gga(s(T19), s(T20), T10)
gcdE_in_gga(s(T51), s(T52), T54) → U6_gga(T51, T52, T54, leA_in_gg(T51, T52))
U6_gga(T51, T52, T54, leA_out_gg(T51, T52)) → U7_gga(T51, T52, T54, addD_in_gag(T51, X55, T52))
addD_in_gag(T72, X91, T73) → U4_gag(T72, X91, T73, addB_in_gag(T72, X91, T73))
addB_in_gag(s(T84), X115, s(T85)) → U2_gag(T84, X115, T85, addB_in_gag(T84, X115, T85))
addB_in_gag(0, T90, T90) → addB_out_gag(0, T90, T90)
U2_gag(T84, X115, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
U4_gag(T72, X91, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U7_gga(T51, T52, T54, addD_out_gag(T51, X55, T52)) → gcdE_out_gga(s(T51), s(T52), T54)
U6_gga(T51, T52, T54, leA_out_gg(T51, T52)) → U8_gga(T51, T52, T54, addD_in_gag(T51, T57, T52))
U8_gga(T51, T52, T54, addD_out_gag(T51, T57, T52)) → U9_gga(T51, T52, T54, gcdE_in_gga(s(T51), T57, T54))
gcdE_in_gga(0, s(T105), s(T105)) → gcdE_out_gga(0, s(T105), s(T105))
gcdE_in_gga(0, 0, 0) → gcdE_out_gga(0, 0, 0)
gcdE_in_gga(T115, T116, T118) → U10_gga(T115, T116, T118, gtC_in_gg(T115, T116))
gtC_in_gg(s(T131), s(T132)) → U3_gg(T131, T132, gtC_in_gg(T131, T132))
gtC_in_gg(s(T137), 0) → gtC_out_gg(s(T137), 0)
U3_gg(T131, T132, gtC_out_gg(T131, T132)) → gtC_out_gg(s(T131), s(T132))
U10_gga(T115, T116, T118, gtC_out_gg(T115, T116)) → gcdE_out_gga(T115, T116, T118)
gcdE_in_gga(T144, 0, T144) → U11_gga(T144, gtC_in_gg(T144, 0))
U11_gga(T144, gtC_out_gg(T144, 0)) → gcdE_out_gga(T144, 0, T144)
gcdE_in_gga(T152, s(T151), T154) → U12_gga(T152, T151, T154, gtC_in_gg(T152, s(T151)))
U12_gga(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U13_gga(T152, T151, T154, addB_in_gag(s(T151), X202, T152))
U13_gga(T152, T151, T154, addB_out_gag(s(T151), X202, T152)) → gcdE_out_gga(T152, s(T151), T154)
U12_gga(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U14_gga(T152, T151, T154, addB_in_gag(s(T151), T157, T152))
U14_gga(T152, T151, T154, addB_out_gag(s(T151), T157, T152)) → U15_gga(T152, T151, T154, gcdE_in_gga(s(T151), T157, T154))
U15_gga(T152, T151, T154, gcdE_out_gga(s(T151), T157, T154)) → gcdE_out_gga(T152, s(T151), T154)
U9_gga(T51, T52, T54, gcdE_out_gga(s(T51), T57, T54)) → gcdE_out_gga(s(T51), s(T52), T54)
GCDE_IN_GGA(s(T19), s(T20), T10) → U5_GGA(T19, T20, T10, leA_in_gg(T19, T20))
GCDE_IN_GGA(s(T19), s(T20), T10) → LEA_IN_GG(T19, T20)
LEA_IN_GG(s(T33), s(T34)) → U1_GG(T33, T34, leA_in_gg(T33, T34))
LEA_IN_GG(s(T33), s(T34)) → LEA_IN_GG(T33, T34)
GCDE_IN_GGA(s(T51), s(T52), T54) → U6_GGA(T51, T52, T54, leA_in_gg(T51, T52))
U6_GGA(T51, T52, T54, leA_out_gg(T51, T52)) → U7_GGA(T51, T52, T54, addD_in_gag(T51, X55, T52))
U6_GGA(T51, T52, T54, leA_out_gg(T51, T52)) → ADDD_IN_GAG(T51, X55, T52)
ADDD_IN_GAG(T72, X91, T73) → U4_GAG(T72, X91, T73, addB_in_gag(T72, X91, T73))
ADDD_IN_GAG(T72, X91, T73) → ADDB_IN_GAG(T72, X91, T73)
ADDB_IN_GAG(s(T84), X115, s(T85)) → U2_GAG(T84, X115, T85, addB_in_gag(T84, X115, T85))
ADDB_IN_GAG(s(T84), X115, s(T85)) → ADDB_IN_GAG(T84, X115, T85)
U6_GGA(T51, T52, T54, leA_out_gg(T51, T52)) → U8_GGA(T51, T52, T54, addD_in_gag(T51, T57, T52))
U8_GGA(T51, T52, T54, addD_out_gag(T51, T57, T52)) → U9_GGA(T51, T52, T54, gcdE_in_gga(s(T51), T57, T54))
U8_GGA(T51, T52, T54, addD_out_gag(T51, T57, T52)) → GCDE_IN_GGA(s(T51), T57, T54)
GCDE_IN_GGA(T115, T116, T118) → U10_GGA(T115, T116, T118, gtC_in_gg(T115, T116))
GCDE_IN_GGA(T115, T116, T118) → GTC_IN_GG(T115, T116)
GTC_IN_GG(s(T131), s(T132)) → U3_GG(T131, T132, gtC_in_gg(T131, T132))
GTC_IN_GG(s(T131), s(T132)) → GTC_IN_GG(T131, T132)
GCDE_IN_GGA(T144, 0, T144) → U11_GGA(T144, gtC_in_gg(T144, 0))
GCDE_IN_GGA(T144, 0, T144) → GTC_IN_GG(T144, 0)
GCDE_IN_GGA(T152, s(T151), T154) → U12_GGA(T152, T151, T154, gtC_in_gg(T152, s(T151)))
GCDE_IN_GGA(T152, s(T151), T154) → GTC_IN_GG(T152, s(T151))
U12_GGA(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U13_GGA(T152, T151, T154, addB_in_gag(s(T151), X202, T152))
U12_GGA(T152, T151, T154, gtC_out_gg(T152, s(T151))) → ADDB_IN_GAG(s(T151), X202, T152)
U12_GGA(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U14_GGA(T152, T151, T154, addB_in_gag(s(T151), T157, T152))
U14_GGA(T152, T151, T154, addB_out_gag(s(T151), T157, T152)) → U15_GGA(T152, T151, T154, gcdE_in_gga(s(T151), T157, T154))
U14_GGA(T152, T151, T154, addB_out_gag(s(T151), T157, T152)) → GCDE_IN_GGA(s(T151), T157, T154)
gcdE_in_gga(s(T19), s(T20), T10) → U5_gga(T19, T20, T10, leA_in_gg(T19, T20))
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
U5_gga(T19, T20, T10, leA_out_gg(T19, T20)) → gcdE_out_gga(s(T19), s(T20), T10)
gcdE_in_gga(s(T51), s(T52), T54) → U6_gga(T51, T52, T54, leA_in_gg(T51, T52))
U6_gga(T51, T52, T54, leA_out_gg(T51, T52)) → U7_gga(T51, T52, T54, addD_in_gag(T51, X55, T52))
addD_in_gag(T72, X91, T73) → U4_gag(T72, X91, T73, addB_in_gag(T72, X91, T73))
addB_in_gag(s(T84), X115, s(T85)) → U2_gag(T84, X115, T85, addB_in_gag(T84, X115, T85))
addB_in_gag(0, T90, T90) → addB_out_gag(0, T90, T90)
U2_gag(T84, X115, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
U4_gag(T72, X91, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U7_gga(T51, T52, T54, addD_out_gag(T51, X55, T52)) → gcdE_out_gga(s(T51), s(T52), T54)
U6_gga(T51, T52, T54, leA_out_gg(T51, T52)) → U8_gga(T51, T52, T54, addD_in_gag(T51, T57, T52))
U8_gga(T51, T52, T54, addD_out_gag(T51, T57, T52)) → U9_gga(T51, T52, T54, gcdE_in_gga(s(T51), T57, T54))
gcdE_in_gga(0, s(T105), s(T105)) → gcdE_out_gga(0, s(T105), s(T105))
gcdE_in_gga(0, 0, 0) → gcdE_out_gga(0, 0, 0)
gcdE_in_gga(T115, T116, T118) → U10_gga(T115, T116, T118, gtC_in_gg(T115, T116))
gtC_in_gg(s(T131), s(T132)) → U3_gg(T131, T132, gtC_in_gg(T131, T132))
gtC_in_gg(s(T137), 0) → gtC_out_gg(s(T137), 0)
U3_gg(T131, T132, gtC_out_gg(T131, T132)) → gtC_out_gg(s(T131), s(T132))
U10_gga(T115, T116, T118, gtC_out_gg(T115, T116)) → gcdE_out_gga(T115, T116, T118)
gcdE_in_gga(T144, 0, T144) → U11_gga(T144, gtC_in_gg(T144, 0))
U11_gga(T144, gtC_out_gg(T144, 0)) → gcdE_out_gga(T144, 0, T144)
gcdE_in_gga(T152, s(T151), T154) → U12_gga(T152, T151, T154, gtC_in_gg(T152, s(T151)))
U12_gga(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U13_gga(T152, T151, T154, addB_in_gag(s(T151), X202, T152))
U13_gga(T152, T151, T154, addB_out_gag(s(T151), X202, T152)) → gcdE_out_gga(T152, s(T151), T154)
U12_gga(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U14_gga(T152, T151, T154, addB_in_gag(s(T151), T157, T152))
U14_gga(T152, T151, T154, addB_out_gag(s(T151), T157, T152)) → U15_gga(T152, T151, T154, gcdE_in_gga(s(T151), T157, T154))
U15_gga(T152, T151, T154, gcdE_out_gga(s(T151), T157, T154)) → gcdE_out_gga(T152, s(T151), T154)
U9_gga(T51, T52, T54, gcdE_out_gga(s(T51), T57, T54)) → gcdE_out_gga(s(T51), s(T52), T54)
GTC_IN_GG(s(T131), s(T132)) → GTC_IN_GG(T131, T132)
gcdE_in_gga(s(T19), s(T20), T10) → U5_gga(T19, T20, T10, leA_in_gg(T19, T20))
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
U5_gga(T19, T20, T10, leA_out_gg(T19, T20)) → gcdE_out_gga(s(T19), s(T20), T10)
gcdE_in_gga(s(T51), s(T52), T54) → U6_gga(T51, T52, T54, leA_in_gg(T51, T52))
U6_gga(T51, T52, T54, leA_out_gg(T51, T52)) → U7_gga(T51, T52, T54, addD_in_gag(T51, X55, T52))
addD_in_gag(T72, X91, T73) → U4_gag(T72, X91, T73, addB_in_gag(T72, X91, T73))
addB_in_gag(s(T84), X115, s(T85)) → U2_gag(T84, X115, T85, addB_in_gag(T84, X115, T85))
addB_in_gag(0, T90, T90) → addB_out_gag(0, T90, T90)
U2_gag(T84, X115, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
U4_gag(T72, X91, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U7_gga(T51, T52, T54, addD_out_gag(T51, X55, T52)) → gcdE_out_gga(s(T51), s(T52), T54)
U6_gga(T51, T52, T54, leA_out_gg(T51, T52)) → U8_gga(T51, T52, T54, addD_in_gag(T51, T57, T52))
U8_gga(T51, T52, T54, addD_out_gag(T51, T57, T52)) → U9_gga(T51, T52, T54, gcdE_in_gga(s(T51), T57, T54))
gcdE_in_gga(0, s(T105), s(T105)) → gcdE_out_gga(0, s(T105), s(T105))
gcdE_in_gga(0, 0, 0) → gcdE_out_gga(0, 0, 0)
gcdE_in_gga(T115, T116, T118) → U10_gga(T115, T116, T118, gtC_in_gg(T115, T116))
gtC_in_gg(s(T131), s(T132)) → U3_gg(T131, T132, gtC_in_gg(T131, T132))
gtC_in_gg(s(T137), 0) → gtC_out_gg(s(T137), 0)
U3_gg(T131, T132, gtC_out_gg(T131, T132)) → gtC_out_gg(s(T131), s(T132))
U10_gga(T115, T116, T118, gtC_out_gg(T115, T116)) → gcdE_out_gga(T115, T116, T118)
gcdE_in_gga(T144, 0, T144) → U11_gga(T144, gtC_in_gg(T144, 0))
U11_gga(T144, gtC_out_gg(T144, 0)) → gcdE_out_gga(T144, 0, T144)
gcdE_in_gga(T152, s(T151), T154) → U12_gga(T152, T151, T154, gtC_in_gg(T152, s(T151)))
U12_gga(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U13_gga(T152, T151, T154, addB_in_gag(s(T151), X202, T152))
U13_gga(T152, T151, T154, addB_out_gag(s(T151), X202, T152)) → gcdE_out_gga(T152, s(T151), T154)
U12_gga(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U14_gga(T152, T151, T154, addB_in_gag(s(T151), T157, T152))
U14_gga(T152, T151, T154, addB_out_gag(s(T151), T157, T152)) → U15_gga(T152, T151, T154, gcdE_in_gga(s(T151), T157, T154))
U15_gga(T152, T151, T154, gcdE_out_gga(s(T151), T157, T154)) → gcdE_out_gga(T152, s(T151), T154)
U9_gga(T51, T52, T54, gcdE_out_gga(s(T51), T57, T54)) → gcdE_out_gga(s(T51), s(T52), T54)
GTC_IN_GG(s(T131), s(T132)) → GTC_IN_GG(T131, T132)
GTC_IN_GG(s(T131), s(T132)) → GTC_IN_GG(T131, T132)
From the DPs we obtained the following set of size-change graphs:
ADDB_IN_GAG(s(T84), X115, s(T85)) → ADDB_IN_GAG(T84, X115, T85)
gcdE_in_gga(s(T19), s(T20), T10) → U5_gga(T19, T20, T10, leA_in_gg(T19, T20))
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
U5_gga(T19, T20, T10, leA_out_gg(T19, T20)) → gcdE_out_gga(s(T19), s(T20), T10)
gcdE_in_gga(s(T51), s(T52), T54) → U6_gga(T51, T52, T54, leA_in_gg(T51, T52))
U6_gga(T51, T52, T54, leA_out_gg(T51, T52)) → U7_gga(T51, T52, T54, addD_in_gag(T51, X55, T52))
addD_in_gag(T72, X91, T73) → U4_gag(T72, X91, T73, addB_in_gag(T72, X91, T73))
addB_in_gag(s(T84), X115, s(T85)) → U2_gag(T84, X115, T85, addB_in_gag(T84, X115, T85))
addB_in_gag(0, T90, T90) → addB_out_gag(0, T90, T90)
U2_gag(T84, X115, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
U4_gag(T72, X91, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U7_gga(T51, T52, T54, addD_out_gag(T51, X55, T52)) → gcdE_out_gga(s(T51), s(T52), T54)
U6_gga(T51, T52, T54, leA_out_gg(T51, T52)) → U8_gga(T51, T52, T54, addD_in_gag(T51, T57, T52))
U8_gga(T51, T52, T54, addD_out_gag(T51, T57, T52)) → U9_gga(T51, T52, T54, gcdE_in_gga(s(T51), T57, T54))
gcdE_in_gga(0, s(T105), s(T105)) → gcdE_out_gga(0, s(T105), s(T105))
gcdE_in_gga(0, 0, 0) → gcdE_out_gga(0, 0, 0)
gcdE_in_gga(T115, T116, T118) → U10_gga(T115, T116, T118, gtC_in_gg(T115, T116))
gtC_in_gg(s(T131), s(T132)) → U3_gg(T131, T132, gtC_in_gg(T131, T132))
gtC_in_gg(s(T137), 0) → gtC_out_gg(s(T137), 0)
U3_gg(T131, T132, gtC_out_gg(T131, T132)) → gtC_out_gg(s(T131), s(T132))
U10_gga(T115, T116, T118, gtC_out_gg(T115, T116)) → gcdE_out_gga(T115, T116, T118)
gcdE_in_gga(T144, 0, T144) → U11_gga(T144, gtC_in_gg(T144, 0))
U11_gga(T144, gtC_out_gg(T144, 0)) → gcdE_out_gga(T144, 0, T144)
gcdE_in_gga(T152, s(T151), T154) → U12_gga(T152, T151, T154, gtC_in_gg(T152, s(T151)))
U12_gga(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U13_gga(T152, T151, T154, addB_in_gag(s(T151), X202, T152))
U13_gga(T152, T151, T154, addB_out_gag(s(T151), X202, T152)) → gcdE_out_gga(T152, s(T151), T154)
U12_gga(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U14_gga(T152, T151, T154, addB_in_gag(s(T151), T157, T152))
U14_gga(T152, T151, T154, addB_out_gag(s(T151), T157, T152)) → U15_gga(T152, T151, T154, gcdE_in_gga(s(T151), T157, T154))
U15_gga(T152, T151, T154, gcdE_out_gga(s(T151), T157, T154)) → gcdE_out_gga(T152, s(T151), T154)
U9_gga(T51, T52, T54, gcdE_out_gga(s(T51), T57, T54)) → gcdE_out_gga(s(T51), s(T52), T54)
ADDB_IN_GAG(s(T84), X115, s(T85)) → ADDB_IN_GAG(T84, X115, T85)
ADDB_IN_GAG(s(T84), s(T85)) → ADDB_IN_GAG(T84, T85)
From the DPs we obtained the following set of size-change graphs:
LEA_IN_GG(s(T33), s(T34)) → LEA_IN_GG(T33, T34)
gcdE_in_gga(s(T19), s(T20), T10) → U5_gga(T19, T20, T10, leA_in_gg(T19, T20))
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
U5_gga(T19, T20, T10, leA_out_gg(T19, T20)) → gcdE_out_gga(s(T19), s(T20), T10)
gcdE_in_gga(s(T51), s(T52), T54) → U6_gga(T51, T52, T54, leA_in_gg(T51, T52))
U6_gga(T51, T52, T54, leA_out_gg(T51, T52)) → U7_gga(T51, T52, T54, addD_in_gag(T51, X55, T52))
addD_in_gag(T72, X91, T73) → U4_gag(T72, X91, T73, addB_in_gag(T72, X91, T73))
addB_in_gag(s(T84), X115, s(T85)) → U2_gag(T84, X115, T85, addB_in_gag(T84, X115, T85))
addB_in_gag(0, T90, T90) → addB_out_gag(0, T90, T90)
U2_gag(T84, X115, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
U4_gag(T72, X91, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U7_gga(T51, T52, T54, addD_out_gag(T51, X55, T52)) → gcdE_out_gga(s(T51), s(T52), T54)
U6_gga(T51, T52, T54, leA_out_gg(T51, T52)) → U8_gga(T51, T52, T54, addD_in_gag(T51, T57, T52))
U8_gga(T51, T52, T54, addD_out_gag(T51, T57, T52)) → U9_gga(T51, T52, T54, gcdE_in_gga(s(T51), T57, T54))
gcdE_in_gga(0, s(T105), s(T105)) → gcdE_out_gga(0, s(T105), s(T105))
gcdE_in_gga(0, 0, 0) → gcdE_out_gga(0, 0, 0)
gcdE_in_gga(T115, T116, T118) → U10_gga(T115, T116, T118, gtC_in_gg(T115, T116))
gtC_in_gg(s(T131), s(T132)) → U3_gg(T131, T132, gtC_in_gg(T131, T132))
gtC_in_gg(s(T137), 0) → gtC_out_gg(s(T137), 0)
U3_gg(T131, T132, gtC_out_gg(T131, T132)) → gtC_out_gg(s(T131), s(T132))
U10_gga(T115, T116, T118, gtC_out_gg(T115, T116)) → gcdE_out_gga(T115, T116, T118)
gcdE_in_gga(T144, 0, T144) → U11_gga(T144, gtC_in_gg(T144, 0))
U11_gga(T144, gtC_out_gg(T144, 0)) → gcdE_out_gga(T144, 0, T144)
gcdE_in_gga(T152, s(T151), T154) → U12_gga(T152, T151, T154, gtC_in_gg(T152, s(T151)))
U12_gga(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U13_gga(T152, T151, T154, addB_in_gag(s(T151), X202, T152))
U13_gga(T152, T151, T154, addB_out_gag(s(T151), X202, T152)) → gcdE_out_gga(T152, s(T151), T154)
U12_gga(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U14_gga(T152, T151, T154, addB_in_gag(s(T151), T157, T152))
U14_gga(T152, T151, T154, addB_out_gag(s(T151), T157, T152)) → U15_gga(T152, T151, T154, gcdE_in_gga(s(T151), T157, T154))
U15_gga(T152, T151, T154, gcdE_out_gga(s(T151), T157, T154)) → gcdE_out_gga(T152, s(T151), T154)
U9_gga(T51, T52, T54, gcdE_out_gga(s(T51), T57, T54)) → gcdE_out_gga(s(T51), s(T52), T54)
LEA_IN_GG(s(T33), s(T34)) → LEA_IN_GG(T33, T34)
LEA_IN_GG(s(T33), s(T34)) → LEA_IN_GG(T33, T34)
From the DPs we obtained the following set of size-change graphs:
GCDE_IN_GGA(s(T51), s(T52), T54) → U6_GGA(T51, T52, T54, leA_in_gg(T51, T52))
U6_GGA(T51, T52, T54, leA_out_gg(T51, T52)) → U8_GGA(T51, T52, T54, addD_in_gag(T51, T57, T52))
U8_GGA(T51, T52, T54, addD_out_gag(T51, T57, T52)) → GCDE_IN_GGA(s(T51), T57, T54)
GCDE_IN_GGA(T152, s(T151), T154) → U12_GGA(T152, T151, T154, gtC_in_gg(T152, s(T151)))
U12_GGA(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U14_GGA(T152, T151, T154, addB_in_gag(s(T151), T157, T152))
U14_GGA(T152, T151, T154, addB_out_gag(s(T151), T157, T152)) → GCDE_IN_GGA(s(T151), T157, T154)
gcdE_in_gga(s(T19), s(T20), T10) → U5_gga(T19, T20, T10, leA_in_gg(T19, T20))
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
U5_gga(T19, T20, T10, leA_out_gg(T19, T20)) → gcdE_out_gga(s(T19), s(T20), T10)
gcdE_in_gga(s(T51), s(T52), T54) → U6_gga(T51, T52, T54, leA_in_gg(T51, T52))
U6_gga(T51, T52, T54, leA_out_gg(T51, T52)) → U7_gga(T51, T52, T54, addD_in_gag(T51, X55, T52))
addD_in_gag(T72, X91, T73) → U4_gag(T72, X91, T73, addB_in_gag(T72, X91, T73))
addB_in_gag(s(T84), X115, s(T85)) → U2_gag(T84, X115, T85, addB_in_gag(T84, X115, T85))
addB_in_gag(0, T90, T90) → addB_out_gag(0, T90, T90)
U2_gag(T84, X115, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
U4_gag(T72, X91, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U7_gga(T51, T52, T54, addD_out_gag(T51, X55, T52)) → gcdE_out_gga(s(T51), s(T52), T54)
U6_gga(T51, T52, T54, leA_out_gg(T51, T52)) → U8_gga(T51, T52, T54, addD_in_gag(T51, T57, T52))
U8_gga(T51, T52, T54, addD_out_gag(T51, T57, T52)) → U9_gga(T51, T52, T54, gcdE_in_gga(s(T51), T57, T54))
gcdE_in_gga(0, s(T105), s(T105)) → gcdE_out_gga(0, s(T105), s(T105))
gcdE_in_gga(0, 0, 0) → gcdE_out_gga(0, 0, 0)
gcdE_in_gga(T115, T116, T118) → U10_gga(T115, T116, T118, gtC_in_gg(T115, T116))
gtC_in_gg(s(T131), s(T132)) → U3_gg(T131, T132, gtC_in_gg(T131, T132))
gtC_in_gg(s(T137), 0) → gtC_out_gg(s(T137), 0)
U3_gg(T131, T132, gtC_out_gg(T131, T132)) → gtC_out_gg(s(T131), s(T132))
U10_gga(T115, T116, T118, gtC_out_gg(T115, T116)) → gcdE_out_gga(T115, T116, T118)
gcdE_in_gga(T144, 0, T144) → U11_gga(T144, gtC_in_gg(T144, 0))
U11_gga(T144, gtC_out_gg(T144, 0)) → gcdE_out_gga(T144, 0, T144)
gcdE_in_gga(T152, s(T151), T154) → U12_gga(T152, T151, T154, gtC_in_gg(T152, s(T151)))
U12_gga(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U13_gga(T152, T151, T154, addB_in_gag(s(T151), X202, T152))
U13_gga(T152, T151, T154, addB_out_gag(s(T151), X202, T152)) → gcdE_out_gga(T152, s(T151), T154)
U12_gga(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U14_gga(T152, T151, T154, addB_in_gag(s(T151), T157, T152))
U14_gga(T152, T151, T154, addB_out_gag(s(T151), T157, T152)) → U15_gga(T152, T151, T154, gcdE_in_gga(s(T151), T157, T154))
U15_gga(T152, T151, T154, gcdE_out_gga(s(T151), T157, T154)) → gcdE_out_gga(T152, s(T151), T154)
U9_gga(T51, T52, T54, gcdE_out_gga(s(T51), T57, T54)) → gcdE_out_gga(s(T51), s(T52), T54)
GCDE_IN_GGA(s(T51), s(T52), T54) → U6_GGA(T51, T52, T54, leA_in_gg(T51, T52))
U6_GGA(T51, T52, T54, leA_out_gg(T51, T52)) → U8_GGA(T51, T52, T54, addD_in_gag(T51, T57, T52))
U8_GGA(T51, T52, T54, addD_out_gag(T51, T57, T52)) → GCDE_IN_GGA(s(T51), T57, T54)
GCDE_IN_GGA(T152, s(T151), T154) → U12_GGA(T152, T151, T154, gtC_in_gg(T152, s(T151)))
U12_GGA(T152, T151, T154, gtC_out_gg(T152, s(T151))) → U14_GGA(T152, T151, T154, addB_in_gag(s(T151), T157, T152))
U14_GGA(T152, T151, T154, addB_out_gag(s(T151), T157, T152)) → GCDE_IN_GGA(s(T151), T157, T154)
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
addD_in_gag(T72, X91, T73) → U4_gag(T72, X91, T73, addB_in_gag(T72, X91, T73))
gtC_in_gg(s(T131), s(T132)) → U3_gg(T131, T132, gtC_in_gg(T131, T132))
addB_in_gag(s(T84), X115, s(T85)) → U2_gag(T84, X115, T85, addB_in_gag(T84, X115, T85))
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
U4_gag(T72, X91, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U3_gg(T131, T132, gtC_out_gg(T131, T132)) → gtC_out_gg(s(T131), s(T132))
U2_gag(T84, X115, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
addB_in_gag(0, T90, T90) → addB_out_gag(0, T90, T90)
gtC_in_gg(s(T137), 0) → gtC_out_gg(s(T137), 0)
GCDE_IN_GGA(s(T51), s(T52)) → U6_GGA(T51, T52, leA_in_gg(T51, T52))
U6_GGA(T51, T52, leA_out_gg(T51, T52)) → U8_GGA(T51, T52, addD_in_gag(T51, T52))
U8_GGA(T51, T52, addD_out_gag(T51, T57, T52)) → GCDE_IN_GGA(s(T51), T57)
GCDE_IN_GGA(T152, s(T151)) → U12_GGA(T152, T151, gtC_in_gg(T152, s(T151)))
U12_GGA(T152, T151, gtC_out_gg(T152, s(T151))) → U14_GGA(T152, T151, addB_in_gag(s(T151), T152))
U14_GGA(T152, T151, addB_out_gag(s(T151), T157, T152)) → GCDE_IN_GGA(s(T151), T157)
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
addD_in_gag(T72, T73) → U4_gag(T72, T73, addB_in_gag(T72, T73))
gtC_in_gg(s(T131), s(T132)) → U3_gg(T131, T132, gtC_in_gg(T131, T132))
addB_in_gag(s(T84), s(T85)) → U2_gag(T84, T85, addB_in_gag(T84, T85))
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
U4_gag(T72, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U3_gg(T131, T132, gtC_out_gg(T131, T132)) → gtC_out_gg(s(T131), s(T132))
U2_gag(T84, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
addB_in_gag(0, T90) → addB_out_gag(0, T90, T90)
gtC_in_gg(s(T137), 0) → gtC_out_gg(s(T137), 0)
leA_in_gg(x0, x1)
addD_in_gag(x0, x1)
gtC_in_gg(x0, x1)
addB_in_gag(x0, x1)
U1_gg(x0, x1, x2)
U4_gag(x0, x1, x2)
U3_gg(x0, x1, x2)
U2_gag(x0, x1, x2)
U6_GGA(T51, T52, leA_out_gg(T51, T52)) → U8_GGA(T51, T52, U4_gag(T51, T52, addB_in_gag(T51, T52)))
GCDE_IN_GGA(s(T51), s(T52)) → U6_GGA(T51, T52, leA_in_gg(T51, T52))
U8_GGA(T51, T52, addD_out_gag(T51, T57, T52)) → GCDE_IN_GGA(s(T51), T57)
GCDE_IN_GGA(T152, s(T151)) → U12_GGA(T152, T151, gtC_in_gg(T152, s(T151)))
U12_GGA(T152, T151, gtC_out_gg(T152, s(T151))) → U14_GGA(T152, T151, addB_in_gag(s(T151), T152))
U14_GGA(T152, T151, addB_out_gag(s(T151), T157, T152)) → GCDE_IN_GGA(s(T151), T157)
U6_GGA(T51, T52, leA_out_gg(T51, T52)) → U8_GGA(T51, T52, U4_gag(T51, T52, addB_in_gag(T51, T52)))
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
addD_in_gag(T72, T73) → U4_gag(T72, T73, addB_in_gag(T72, T73))
gtC_in_gg(s(T131), s(T132)) → U3_gg(T131, T132, gtC_in_gg(T131, T132))
addB_in_gag(s(T84), s(T85)) → U2_gag(T84, T85, addB_in_gag(T84, T85))
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
U4_gag(T72, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U3_gg(T131, T132, gtC_out_gg(T131, T132)) → gtC_out_gg(s(T131), s(T132))
U2_gag(T84, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
addB_in_gag(0, T90) → addB_out_gag(0, T90, T90)
gtC_in_gg(s(T137), 0) → gtC_out_gg(s(T137), 0)
leA_in_gg(x0, x1)
addD_in_gag(x0, x1)
gtC_in_gg(x0, x1)
addB_in_gag(x0, x1)
U1_gg(x0, x1, x2)
U4_gag(x0, x1, x2)
U3_gg(x0, x1, x2)
U2_gag(x0, x1, x2)
GCDE_IN_GGA(s(T51), s(T52)) → U6_GGA(T51, T52, leA_in_gg(T51, T52))
U8_GGA(T51, T52, addD_out_gag(T51, T57, T52)) → GCDE_IN_GGA(s(T51), T57)
GCDE_IN_GGA(T152, s(T151)) → U12_GGA(T152, T151, gtC_in_gg(T152, s(T151)))
U12_GGA(T152, T151, gtC_out_gg(T152, s(T151))) → U14_GGA(T152, T151, addB_in_gag(s(T151), T152))
U14_GGA(T152, T151, addB_out_gag(s(T151), T157, T152)) → GCDE_IN_GGA(s(T151), T157)
U6_GGA(T51, T52, leA_out_gg(T51, T52)) → U8_GGA(T51, T52, U4_gag(T51, T52, addB_in_gag(T51, T52)))
addB_in_gag(s(T84), s(T85)) → U2_gag(T84, T85, addB_in_gag(T84, T85))
addB_in_gag(0, T90) → addB_out_gag(0, T90, T90)
U4_gag(T72, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U2_gag(T84, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
gtC_in_gg(s(T131), s(T132)) → U3_gg(T131, T132, gtC_in_gg(T131, T132))
gtC_in_gg(s(T137), 0) → gtC_out_gg(s(T137), 0)
U3_gg(T131, T132, gtC_out_gg(T131, T132)) → gtC_out_gg(s(T131), s(T132))
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
leA_in_gg(x0, x1)
addD_in_gag(x0, x1)
gtC_in_gg(x0, x1)
addB_in_gag(x0, x1)
U1_gg(x0, x1, x2)
U4_gag(x0, x1, x2)
U3_gg(x0, x1, x2)
U2_gag(x0, x1, x2)
addD_in_gag(x0, x1)
GCDE_IN_GGA(s(T51), s(T52)) → U6_GGA(T51, T52, leA_in_gg(T51, T52))
U8_GGA(T51, T52, addD_out_gag(T51, T57, T52)) → GCDE_IN_GGA(s(T51), T57)
GCDE_IN_GGA(T152, s(T151)) → U12_GGA(T152, T151, gtC_in_gg(T152, s(T151)))
U12_GGA(T152, T151, gtC_out_gg(T152, s(T151))) → U14_GGA(T152, T151, addB_in_gag(s(T151), T152))
U14_GGA(T152, T151, addB_out_gag(s(T151), T157, T152)) → GCDE_IN_GGA(s(T151), T157)
U6_GGA(T51, T52, leA_out_gg(T51, T52)) → U8_GGA(T51, T52, U4_gag(T51, T52, addB_in_gag(T51, T52)))
addB_in_gag(s(T84), s(T85)) → U2_gag(T84, T85, addB_in_gag(T84, T85))
addB_in_gag(0, T90) → addB_out_gag(0, T90, T90)
U4_gag(T72, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U2_gag(T84, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
gtC_in_gg(s(T131), s(T132)) → U3_gg(T131, T132, gtC_in_gg(T131, T132))
gtC_in_gg(s(T137), 0) → gtC_out_gg(s(T137), 0)
U3_gg(T131, T132, gtC_out_gg(T131, T132)) → gtC_out_gg(s(T131), s(T132))
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
leA_in_gg(x0, x1)
gtC_in_gg(x0, x1)
addB_in_gag(x0, x1)
U1_gg(x0, x1, x2)
U4_gag(x0, x1, x2)
U3_gg(x0, x1, x2)
U2_gag(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U12_GGA(T152, T151, gtC_out_gg(T152, s(T151))) → U14_GGA(T152, T151, addB_in_gag(s(T151), T152))
POL(0) = 0
POL(GCDE_IN_GGA(x1, x2)) = x1
POL(U12_GGA(x1, x2, x3)) = x3
POL(U14_GGA(x1, x2, x3)) = 1 + x2
POL(U1_gg(x1, x2, x3)) = 0
POL(U2_gag(x1, x2, x3)) = 0
POL(U3_gg(x1, x2, x3)) = 1 + x3
POL(U4_gag(x1, x2, x3)) = 0
POL(U6_GGA(x1, x2, x3)) = 1 + x1
POL(U8_GGA(x1, x2, x3)) = 1 + x1
POL(addB_in_gag(x1, x2)) = 0
POL(addB_out_gag(x1, x2, x3)) = 0
POL(addD_out_gag(x1, x2, x3)) = 0
POL(gtC_in_gg(x1, x2)) = x1
POL(gtC_out_gg(x1, x2)) = 1 + x2
POL(leA_in_gg(x1, x2)) = 0
POL(leA_out_gg(x1, x2)) = 0
POL(s(x1)) = 1 + x1
gtC_in_gg(s(T131), s(T132)) → U3_gg(T131, T132, gtC_in_gg(T131, T132))
gtC_in_gg(s(T137), 0) → gtC_out_gg(s(T137), 0)
U3_gg(T131, T132, gtC_out_gg(T131, T132)) → gtC_out_gg(s(T131), s(T132))
GCDE_IN_GGA(s(T51), s(T52)) → U6_GGA(T51, T52, leA_in_gg(T51, T52))
U8_GGA(T51, T52, addD_out_gag(T51, T57, T52)) → GCDE_IN_GGA(s(T51), T57)
GCDE_IN_GGA(T152, s(T151)) → U12_GGA(T152, T151, gtC_in_gg(T152, s(T151)))
U14_GGA(T152, T151, addB_out_gag(s(T151), T157, T152)) → GCDE_IN_GGA(s(T151), T157)
U6_GGA(T51, T52, leA_out_gg(T51, T52)) → U8_GGA(T51, T52, U4_gag(T51, T52, addB_in_gag(T51, T52)))
addB_in_gag(s(T84), s(T85)) → U2_gag(T84, T85, addB_in_gag(T84, T85))
addB_in_gag(0, T90) → addB_out_gag(0, T90, T90)
U4_gag(T72, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U2_gag(T84, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
gtC_in_gg(s(T131), s(T132)) → U3_gg(T131, T132, gtC_in_gg(T131, T132))
gtC_in_gg(s(T137), 0) → gtC_out_gg(s(T137), 0)
U3_gg(T131, T132, gtC_out_gg(T131, T132)) → gtC_out_gg(s(T131), s(T132))
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
leA_in_gg(x0, x1)
gtC_in_gg(x0, x1)
addB_in_gag(x0, x1)
U1_gg(x0, x1, x2)
U4_gag(x0, x1, x2)
U3_gg(x0, x1, x2)
U2_gag(x0, x1, x2)
U6_GGA(T51, T52, leA_out_gg(T51, T52)) → U8_GGA(T51, T52, U4_gag(T51, T52, addB_in_gag(T51, T52)))
U8_GGA(T51, T52, addD_out_gag(T51, T57, T52)) → GCDE_IN_GGA(s(T51), T57)
GCDE_IN_GGA(s(T51), s(T52)) → U6_GGA(T51, T52, leA_in_gg(T51, T52))
addB_in_gag(s(T84), s(T85)) → U2_gag(T84, T85, addB_in_gag(T84, T85))
addB_in_gag(0, T90) → addB_out_gag(0, T90, T90)
U4_gag(T72, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U2_gag(T84, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
gtC_in_gg(s(T131), s(T132)) → U3_gg(T131, T132, gtC_in_gg(T131, T132))
gtC_in_gg(s(T137), 0) → gtC_out_gg(s(T137), 0)
U3_gg(T131, T132, gtC_out_gg(T131, T132)) → gtC_out_gg(s(T131), s(T132))
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
leA_in_gg(x0, x1)
gtC_in_gg(x0, x1)
addB_in_gag(x0, x1)
U1_gg(x0, x1, x2)
U4_gag(x0, x1, x2)
U3_gg(x0, x1, x2)
U2_gag(x0, x1, x2)
U6_GGA(T51, T52, leA_out_gg(T51, T52)) → U8_GGA(T51, T52, U4_gag(T51, T52, addB_in_gag(T51, T52)))
U8_GGA(T51, T52, addD_out_gag(T51, T57, T52)) → GCDE_IN_GGA(s(T51), T57)
GCDE_IN_GGA(s(T51), s(T52)) → U6_GGA(T51, T52, leA_in_gg(T51, T52))
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
addB_in_gag(s(T84), s(T85)) → U2_gag(T84, T85, addB_in_gag(T84, T85))
addB_in_gag(0, T90) → addB_out_gag(0, T90, T90)
U4_gag(T72, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U2_gag(T84, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
leA_in_gg(x0, x1)
gtC_in_gg(x0, x1)
addB_in_gag(x0, x1)
U1_gg(x0, x1, x2)
U4_gag(x0, x1, x2)
U3_gg(x0, x1, x2)
U2_gag(x0, x1, x2)
gtC_in_gg(x0, x1)
U3_gg(x0, x1, x2)
U6_GGA(T51, T52, leA_out_gg(T51, T52)) → U8_GGA(T51, T52, U4_gag(T51, T52, addB_in_gag(T51, T52)))
U8_GGA(T51, T52, addD_out_gag(T51, T57, T52)) → GCDE_IN_GGA(s(T51), T57)
GCDE_IN_GGA(s(T51), s(T52)) → U6_GGA(T51, T52, leA_in_gg(T51, T52))
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
addB_in_gag(s(T84), s(T85)) → U2_gag(T84, T85, addB_in_gag(T84, T85))
addB_in_gag(0, T90) → addB_out_gag(0, T90, T90)
U4_gag(T72, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U2_gag(T84, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
leA_in_gg(x0, x1)
addB_in_gag(x0, x1)
U1_gg(x0, x1, x2)
U4_gag(x0, x1, x2)
U2_gag(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
GCDE_IN_GGA(s(T51), s(T52)) → U6_GGA(T51, T52, leA_in_gg(T51, T52))
POL(0) = 0
POL(GCDE_IN_GGA(x1, x2)) = x2
POL(U1_gg(x1, x2, x3)) = 0
POL(U2_gag(x1, x2, x3)) = x3
POL(U4_gag(x1, x2, x3)) = x3
POL(U6_GGA(x1, x2, x3)) = x2
POL(U8_GGA(x1, x2, x3)) = x3
POL(addB_in_gag(x1, x2)) = x2
POL(addB_out_gag(x1, x2, x3)) = x2
POL(addD_out_gag(x1, x2, x3)) = x2
POL(leA_in_gg(x1, x2)) = 0
POL(leA_out_gg(x1, x2)) = 0
POL(s(x1)) = 1 + x1
addB_in_gag(s(T84), s(T85)) → U2_gag(T84, T85, addB_in_gag(T84, T85))
addB_in_gag(0, T90) → addB_out_gag(0, T90, T90)
U4_gag(T72, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U2_gag(T84, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
U6_GGA(T51, T52, leA_out_gg(T51, T52)) → U8_GGA(T51, T52, U4_gag(T51, T52, addB_in_gag(T51, T52)))
U8_GGA(T51, T52, addD_out_gag(T51, T57, T52)) → GCDE_IN_GGA(s(T51), T57)
leA_in_gg(s(T33), s(T34)) → U1_gg(T33, T34, leA_in_gg(T33, T34))
leA_in_gg(0, s(T41)) → leA_out_gg(0, s(T41))
leA_in_gg(0, 0) → leA_out_gg(0, 0)
U1_gg(T33, T34, leA_out_gg(T33, T34)) → leA_out_gg(s(T33), s(T34))
addB_in_gag(s(T84), s(T85)) → U2_gag(T84, T85, addB_in_gag(T84, T85))
addB_in_gag(0, T90) → addB_out_gag(0, T90, T90)
U4_gag(T72, T73, addB_out_gag(T72, X91, T73)) → addD_out_gag(T72, X91, T73)
U2_gag(T84, T85, addB_out_gag(T84, X115, T85)) → addB_out_gag(s(T84), X115, s(T85))
leA_in_gg(x0, x1)
addB_in_gag(x0, x1)
U1_gg(x0, x1, x2)
U4_gag(x0, x1, x2)
U2_gag(x0, x1, x2)